MA:MsgA, s:MA.state, k:Knd, l:IdLnk, vaal:MA.V(k).
<k,l>  dom(1of(2of(2of(2of(2of(2of(MA)))))))
 (filter(ms.eqof(IdLnkDeq)(mlnk(ms),l);MA.sends(k,s,vaal)) ~ nil) 

latex

Definitions

b, Valtype(da;k), M.V(k), M.state, MsgA, t  T, Knd, IdLnk, A, P  Q, x:A. B(x), M.sends(k,s,v), 1of(t), KindDeq, eqof(d), IdLnkDeq, product-deq(A;B;a;b), fpf-vals(eq;P;f), 2of(t), tagged-messages(l;s;v;L), map(f;as), concat(ll), mlnk(m), filter(P;l), x  dom(f), x(s), State(ds), x(s1,s2), Id, a:A fp B(a), , x. t(x), Top, A List, tagged-list-messages(s;v;L), P  Q, P & Q, P  Q, S  T, f o g, b, Prop, Unit, False, p  q, rcv(l,tg), f(x)?z

Lemmas

fpf-cap wf, rcv wf, ma-valtype wf, fpf-vals-nil, band wf, assert of band, filter-fpf-vals, subtype rel list, subtype rel product, tagged-list-messages wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, map-map, top wf, concat wf, deq property, subtype rel self, not wf, fpf-dom wf, product-deq wf, Kind-deq wf, idlnk-deq wf, fpf-trivial-subtype-top, fpf wf, ma-state wf, Knd wf, IdLnk wf, filter-concat, map wf, Id wf, pi2 wf, assert wf, fpf-vals wf, eqof wf, pi1 wf, msga wf